00100	EXPR PROPSUBST(TERM,VAR,EXP);
00200	     PROPSUBST1(TERM,VAR,EXP,MAKERNL(FREEVARS TERM,ALLVARS EXP));
00300	
00400	EXPR PROPSUBST1(TERM,VAR,EXP,RNL);
00500	     IF ATOM EXP
00600	     THEN IF ISVAR EXP
00700		  THEN IF EXP=VAR THEN TERM ELSE EXP
00800		  ELSE EXP
00900	     ELSE IF ¬ATOM CAR EXP ∧ ISQUANT CAAR EXP
01000		  THEN IF CADAR EXP=VAR THEN EXP
01100		  ELSE BEGIN SCALAR NEWNAM;
01200			     NEWNAM←ASSOC(CADAR EXP,RNL);
01300			     NEWNAM←IF NULL NEWNAM
01400				    THEN CADAR EXP
01500				    ELSE CDR NEWNAM;
01600			     RETURN LIST(LIST(CAAR EXP,NEWNAM),
01700					 PROPSUBST1(TERM,
01800						    VAR,
01900						    SUBST(NEWNAM,
02000							  CADAR EXP,
02100							  CADR EXP),
02200						    RNL));
02300		       END
02400		  ELSE PROPSUBST1(TERM,VAR,CAR EXP,RNL)
02500		       .PROPSUBSTL(TERM,VAR,CDR EXP,RNL);
02600	
02700	EXPR PROPSUBSTL(TERM,VAR,EXPL,RNL);
02800	     IF NULL EXPL THEN NIL ELSE
02900	     PROPSUBST1(TERM,VAR,CAR EXPL,RNL).PROPSUBSTL(TERM,VAR,CDR EXPL,RNL);
03000